(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
f(X) → if(X, c, n__f(n__true))
if(true, X, Y) → X
if(false, X, Y) → activate(Y)
f(X) → n__f(X)
true → n__true
activate(n__f(X)) → f(activate(X))
activate(n__true) → true
activate(X) → X
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 4.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
c0() → 0
n__f0(0) → 0
n__true0() → 0
false0() → 0
f0(0) → 1
if0(0, 0, 0) → 2
true0() → 3
activate0(0) → 4
c1() → 5
n__true1() → 7
n__f1(7) → 6
if1(0, 5, 6) → 1
activate1(0) → 2
n__f1(0) → 1
n__true1() → 3
activate1(0) → 8
f1(8) → 4
true1() → 4
c2() → 9
n__true2() → 11
n__f2(11) → 10
if2(8, 9, 10) → 4
activate1(6) → 1
n__f2(8) → 4
n__true2() → 4
f1(8) → 2
f1(8) → 8
true1() → 2
true1() → 8
if2(8, 9, 10) → 2
if2(8, 9, 10) → 8
n__f2(8) → 2
n__f2(8) → 8
n__true2() → 2
n__true2() → 8
activate2(7) → 12
f2(12) → 1
activate1(10) → 4
activate1(10) → 2
activate1(10) → 8
activate2(11) → 12
f2(12) → 4
c3() → 13
n__true3() → 15
n__f3(15) → 14
if3(12, 13, 14) → 1
n__f3(12) → 1
true2() → 12
f2(12) → 2
f2(12) → 8
if3(12, 13, 14) → 4
n__f3(12) → 4
true3() → 12
n__true3() → 12
if3(12, 13, 14) → 2
if3(12, 13, 14) → 8
n__f3(12) → 2
n__f3(12) → 8
n__true4() → 12
0 → 4
0 → 2
0 → 8
6 → 1
9 → 4
9 → 2
9 → 8
10 → 4
10 → 2
10 → 8
7 → 12
11 → 12
13 → 1
13 → 4
13 → 2
13 → 8
(2) BOUNDS(1, n^1)